<!DOCTYPE HTML PUBLIC "-//W3C//DTD HTML 4.01 Transitional//EN" "http://www.w3.org/TR/html4/loose.dtd">
<!-- NewPage -->
<html lang="en">
<head>
<title>DjVars</title>
<link rel="stylesheet" type="text/css" href="../../stylesheet.css" title="Style">
</head>
<body>
<script type="text/javascript"><!--
    if (location.href.indexOf('is-external=true') == -1) {
        parent.document.title="DjVars";
    }
//-->
</script>
<noscript>
<div>JavaScript is disabled on your browser.</div>
</noscript>
<!-- ========= START OF TOP NAVBAR ======= -->
<div class="topNav"><a name="navbar_top">
<!--   -->
</a><a href="#skip-navbar_top" title="Skip navigation links"></a><a name="navbar_top_firstrow">
<!--   -->
</a>
<ul class="navList" title="Navigation">
<li><a href="../../overview-summary.html">Overview</a></li>
<li><a href="package-summary.html">Package</a></li>
<li class="navBarCell1Rev">Class</li>
<li><a href="package-tree.html">Tree</a></li>
<li><a href="../../deprecated-list.html">Deprecated</a></li>
<li><a href="../../index-all.html">Index</a></li>
<li><a href="../../help-doc.html">Help</a></li>
</ul>
</div>
<div class="subNav">
<ul class="navList">
<li><a href="../../mmj/lang/Cnst.html" title="class in mmj.lang"><span class="strong">Prev Class</span></a></li>
<li><a href="../../mmj/lang/Formula.html" title="class in mmj.lang"><span class="strong">Next Class</span></a></li>
</ul>
<ul class="navList">
<li><a href="../../index.html?mmj/lang/DjVars.html" target="_top">Frames</a></li>
<li><a href="DjVars.html" target="_top">No Frames</a></li>
</ul>
<ul class="navList" id="allclasses_navbar_top">
<li><a href="../../allclasses-noframe.html">All Classes</a></li>
</ul>
<div>
<script type="text/javascript"><!--
  allClassesLink = document.getElementById("allclasses_navbar_top");
  if(window==top) {
    allClassesLink.style.display = "block";
  }
  else {
    allClassesLink.style.display = "none";
  }
  //-->
</script>
</div>
<div>
<ul class="subNavList">
<li>Summary:&nbsp;</li>
<li>Nested&nbsp;|&nbsp;</li>
<li><a href="#field_summary">Field</a>&nbsp;|&nbsp;</li>
<li><a href="#constructor_summary">Constr</a>&nbsp;|&nbsp;</li>
<li><a href="#method_summary">Method</a></li>
</ul>
<ul class="subNavList">
<li>Detail:&nbsp;</li>
<li><a href="#field_detail">Field</a>&nbsp;|&nbsp;</li>
<li><a href="#constructor_detail">Constr</a>&nbsp;|&nbsp;</li>
<li><a href="#method_detail">Method</a></li>
</ul>
</div>
<a name="skip-navbar_top">
<!--   -->
</a></div>
<!-- ========= END OF TOP NAVBAR ========= -->
<!-- ======== START OF CLASS DATA ======== -->
<div class="header">
<div class="subTitle">mmj.lang</div>
<h2 title="Class DjVars" class="title">Class DjVars</h2>
</div>
<div class="contentContainer">
<ul class="inheritance">
<li>java.lang.Object</li>
<li>
<ul class="inheritance">
<li>mmj.lang.DjVars</li>
</ul>
</li>
</ul>
<div class="description">
<ul class="blockList">
<li class="blockList">
<dl>
<dt>All Implemented Interfaces:</dt>
<dd>java.lang.Comparable&lt;<a href="../../mmj/lang/DjVars.html" title="class in mmj.lang">DjVars</a>&gt;</dd>
</dl>
<hr>
<br>
<pre>public class <span class="strong">DjVars</span>
extends java.lang.Object
implements java.lang.Comparable&lt;<a href="../../mmj/lang/DjVars.html" title="class in mmj.lang">DjVars</a>&gt;</pre>
<div class="block">DjVars is a simple structure that holds a pair of variables specified in a
 Metamath $d statement, the "Disjoint Variable Restriction" statement.
 "Disjoint" here means different. See Pg. 96 of Metamath.pdf. Refer also to
 mmj.verify.VerifyProofs.java, which is where DjVars really come into play.
 The narrative version is tricky and tedious, and is not repeated here...
 Another minor complication is that Metamath's "$d" statement employs a
 shorthand notation allowing several variable to be specified on a single $d
 statement. This results in multiple DjVars objects since each pair
 combination in the $d must be treated as a separate restriction (the
 combinatorial explosion is exciting when there are many variables listed!)
 Also, multiple $d statements are allowed to have overlapping pairs, perhaps
 resulting from the combinatorial explosions. This all makes it easy for the
 person writing the Metamath .mm file, but there is some work storing the
 results. During loading of LogicalSystem, DjVars are maintained in
 mmj.lang.ScopeDef.java -- actually, a list of ScopeDef's. And DjVars are
 stored in mmj.lang.ScopeFrame.java and mmj.lang.OptFrame.java as part of a
 successful system load operation.</div>
<dl><dt><span class="strong">See Also:</span></dt><dd><a href="../../MetamathERNotes.html"> Nomenclature and
      Entity-Relationship Notes</a></dd></dl>
</li>
</ul>
</div>
<div class="summary">
<ul class="blockList">
<li class="blockList">
<!-- =========== FIELD SUMMARY =========== -->
<ul class="blockList">
<li class="blockList"><a name="field_summary">
<!--   -->
</a>
<h3>Field Summary</h3>
<table class="overviewSummary" border="0" cellpadding="3" cellspacing="0" summary="Field Summary table, listing fields, and an explanation">
<caption><span>Fields</span><span class="tabEnd">&nbsp;</span></caption>
<tr>
<th class="colFirst" scope="col">Modifier and Type</th>
<th class="colLast" scope="col">Field and Description</th>
</tr>
<tr class="altColor">
<td class="colFirst"><code>static java.util.Comparator&lt;? super <a href="../../mmj/lang/Var.html" title="class in mmj.lang">Var</a>&gt;</code></td>
<td class="colLast"><code><strong><a href="../../mmj/lang/DjVars.html#DV_ORDER">DV_ORDER</a></strong></code>
<div class="block">This is the ordering that will be used to determine which variable in a
 DjVars is "hi" and which is "lo", and is visible to the user as the
 ordering of variables in missing $d statmements generated by the program.</div>
</td>
</tr>
</table>
</li>
</ul>
<!-- ======== CONSTRUCTOR SUMMARY ======== -->
<ul class="blockList">
<li class="blockList"><a name="constructor_summary">
<!--   -->
</a>
<h3>Constructor Summary</h3>
<table class="overviewSummary" border="0" cellpadding="3" cellspacing="0" summary="Constructor Summary table, listing constructors, and an explanation">
<caption><span>Constructors</span><span class="tabEnd">&nbsp;</span></caption>
<tr>
<th class="colOne" scope="col">Constructor and Description</th>
</tr>
<tr class="altColor">
<td class="colOne"><code><strong><a href="../../mmj/lang/DjVars.html#DjVars(java.util.Map, java.lang.String, java.lang.String)">DjVars</a></strong>(java.util.Map&lt;java.lang.String,<a href="../../mmj/lang/Sym.html" title="class in mmj.lang">Sym</a>&gt;&nbsp;symTbl,
      java.lang.String&nbsp;loS,
      java.lang.String&nbsp;hiS)</code>
<div class="block">Construct using two Var id Strings.</div>
</td>
</tr>
<tr class="rowColor">
<td class="colOne"><code><strong><a href="../../mmj/lang/DjVars.html#DjVars(mmj.lang.Var, mmj.lang.Var)">DjVars</a></strong>(<a href="../../mmj/lang/Var.html" title="class in mmj.lang">Var</a>&nbsp;lo,
      <a href="../../mmj/lang/Var.html" title="class in mmj.lang">Var</a>&nbsp;hi)</code>
<div class="block">Construct using two Var's.</div>
</td>
</tr>
</table>
</li>
</ul>
<!-- ========== METHOD SUMMARY =========== -->
<ul class="blockList">
<li class="blockList"><a name="method_summary">
<!--   -->
</a>
<h3>Method Summary</h3>
<table class="overviewSummary" border="0" cellpadding="3" cellspacing="0" summary="Method Summary table, listing methods, and an explanation">
<caption><span>Methods</span><span class="tabEnd">&nbsp;</span></caption>
<tr>
<th class="colFirst" scope="col">Modifier and Type</th>
<th class="colLast" scope="col">Method and Description</th>
</tr>
<tr class="altColor">
<td class="colFirst"><code>static boolean</code></td>
<td class="colLast"><code><strong><a href="../../mmj/lang/DjVars.html#areBothDjVarsInExtendedFrame(mmj.lang.DjVars, mmj.lang.ScopeFrame, mmj.lang.ScopeFrame)">areBothDjVarsInExtendedFrame</a></strong>(<a href="../../mmj/lang/DjVars.html" title="class in mmj.lang">DjVars</a>&nbsp;djVars,
                            <a href="../../mmj/lang/ScopeFrame.html" title="class in mmj.lang">ScopeFrame</a>&nbsp;mandFrame,
                            <a href="../../mmj/lang/ScopeFrame.html" title="class in mmj.lang">ScopeFrame</a>&nbsp;optFrame)</code>
<div class="block">Helper routine for Theorem Loader to confirm that both DjVars variables
 are in the Extended Frame of a theorem.</div>
</td>
</tr>
<tr class="rowColor">
<td class="colFirst"><code>static java.util.List&lt;java.lang.StringBuilder&gt;</code></td>
<td class="colLast"><code><strong><a href="../../mmj/lang/DjVars.html#buildMetamathDjVarsStatementList(mmj.pa.DistinctVariablesStmt[])">buildMetamathDjVarsStatementList</a></strong>(<a href="../../mmj/pa/DistinctVariablesStmt.html" title="class in mmj.pa">DistinctVariablesStmt</a>[]&nbsp;distinctVariablesStmtArray)</code>
<div class="block">Builds a LinkedList of StringBuilders containing the Metamath formatted
 text $d statements for the theorem.</div>
</td>
</tr>
<tr class="altColor">
<td class="colFirst"><code>static java.util.List&lt;java.lang.StringBuilder&gt;</code></td>
<td class="colLast"><code><strong><a href="../../mmj/lang/DjVars.html#buildMetamathDjVarsStatementList(mmj.lang.Theorem)">buildMetamathDjVarsStatementList</a></strong>(<a href="../../mmj/lang/Theorem.html" title="class in mmj.lang">Theorem</a>&nbsp;theorem)</code>
<div class="block">Builds a LinkedList of StringBuilders containing the Metamath format text
 $d statements for the theorem.</div>
</td>
</tr>
<tr class="rowColor">
<td class="colFirst"><code>int</code></td>
<td class="colLast"><code><strong><a href="../../mmj/lang/DjVars.html#compareTo(mmj.lang.DjVars)">compareTo</a></strong>(<a href="../../mmj/lang/DjVars.html" title="class in mmj.lang">DjVars</a>&nbsp;obj)</code>
<div class="block">Compares DjVars object based on the variables.</div>
</td>
</tr>
<tr class="altColor">
<td class="colFirst"><code>static java.util.List&lt;java.lang.StringBuilder&gt;</code></td>
<td class="colLast"><code><strong><a href="../../mmj/lang/DjVars.html#convertDvGroupsListToMetamathList(java.util.List)">convertDvGroupsListToMetamathList</a></strong>(java.util.List&lt;java.util.List&lt;<a href="../../mmj/lang/Var.html" title="class in mmj.lang">Var</a>&gt;&gt;&nbsp;comboDvGroups)</code>
<div class="block">Converts a ArrayList of Lists containing distinct variables into a
 LinkedList of StringBuilders containing Metamath format text $d
 statements.</div>
</td>
</tr>
<tr class="rowColor">
<td class="colFirst"><code>boolean</code></td>
<td class="colLast"><code><strong><a href="../../mmj/lang/DjVars.html#equals(java.lang.Object)">equals</a></strong>(java.lang.Object&nbsp;obj)</code>&nbsp;</td>
</tr>
<tr class="altColor">
<td class="colFirst"><code><a href="../../mmj/lang/Var.html" title="class in mmj.lang">Var</a></code></td>
<td class="colLast"><code><strong><a href="../../mmj/lang/DjVars.html#getVarHi()">getVarHi</a></strong>()</code>
<div class="block">Return the "high" Dj Var, varHi.</div>
</td>
</tr>
<tr class="rowColor">
<td class="colFirst"><code><a href="../../mmj/lang/Var.html" title="class in mmj.lang">Var</a></code></td>
<td class="colLast"><code><strong><a href="../../mmj/lang/DjVars.html#getVarLo()">getVarLo</a></strong>()</code>
<div class="block">Return the "low" Dj Var, varLo.</div>
</td>
</tr>
<tr class="altColor">
<td class="colFirst"><code>int</code></td>
<td class="colLast"><code><strong><a href="../../mmj/lang/DjVars.html#hashCode()">hashCode</a></strong>()</code>&nbsp;</td>
</tr>
<tr class="rowColor">
<td class="colFirst"><code>static boolean</code></td>
<td class="colLast"><code><strong><a href="../../mmj/lang/DjVars.html#isDjVarsVarInExtendedFrame(mmj.lang.Var, mmj.lang.ScopeFrame, mmj.lang.ScopeFrame)">isDjVarsVarInExtendedFrame</a></strong>(<a href="../../mmj/lang/Var.html" title="class in mmj.lang">Var</a>&nbsp;djVarsVar,
                          <a href="../../mmj/lang/ScopeFrame.html" title="class in mmj.lang">ScopeFrame</a>&nbsp;mandFrame,
                          <a href="../../mmj/lang/ScopeFrame.html" title="class in mmj.lang">ScopeFrame</a>&nbsp;optFrame)</code>
<div class="block">Helper routine for Proof Assistant to confirm that a DjVars variable is
 defined in the Theorem's Extended Frame.</div>
</td>
</tr>
<tr class="altColor">
<td class="colFirst"><code>void</code></td>
<td class="colLast"><code><strong><a href="../../mmj/lang/DjVars.html#set(mmj.lang.Var, mmj.lang.Var)">set</a></strong>(<a href="../../mmj/lang/Var.html" title="class in mmj.lang">Var</a>&nbsp;lo,
   <a href="../../mmj/lang/Var.html" title="class in mmj.lang">Var</a>&nbsp;hi)</code>
<div class="block">Set the contents of this DjVars object.</div>
</td>
</tr>
<tr class="rowColor">
<td class="colFirst"><code>static <a href="../../mmj/lang/DjVars.html" title="class in mmj.lang">DjVars</a>[]</code></td>
<td class="colLast"><code><strong><a href="../../mmj/lang/DjVars.html#sortAndCombineDvArrays(mmj.lang.DjVars[], mmj.lang.DjVars[])">sortAndCombineDvArrays</a></strong>(<a href="../../mmj/lang/DjVars.html" title="class in mmj.lang">DjVars</a>[]&nbsp;array1,
                      <a href="../../mmj/lang/DjVars.html" title="class in mmj.lang">DjVars</a>[]&nbsp;array2)</code>
<div class="block">Merges two arrays of DjVars returning a single array in ascending
 compareTo order with duplicates eliminated.</div>
</td>
</tr>
<tr class="altColor">
<td class="colFirst"><code>static <a href="../../mmj/lang/DjVars.html" title="class in mmj.lang">DjVars</a>[]</code></td>
<td class="colLast"><code><strong><a href="../../mmj/lang/DjVars.html#sortAndCombineDvListOfLists(java.util.List)">sortAndCombineDvListOfLists</a></strong>(java.util.List&lt;java.util.List&lt;<a href="../../mmj/lang/DjVars.html" title="class in mmj.lang">DjVars</a>&gt;&gt;&nbsp;list1)</code>
<div class="block">Merges lists of lists of DjVars returning a single array in ascending
 compareTo order with duplicates eliminated.</div>
</td>
</tr>
<tr class="rowColor">
<td class="colFirst"><code>java.lang.String</code></td>
<td class="colLast"><code><strong><a href="../../mmj/lang/DjVars.html#toString()">toString</a></strong>()</code>
<div class="block">Converts DjVars to String.</div>
</td>
</tr>
</table>
<ul class="blockList">
<li class="blockList"><a name="methods_inherited_from_class_java.lang.Object">
<!--   -->
</a>
<h3>Methods inherited from class&nbsp;java.lang.Object</h3>
<code>clone, finalize, getClass, notify, notifyAll, wait, wait, wait</code></li>
</ul>
</li>
</ul>
</li>
</ul>
</div>
<div class="details">
<ul class="blockList">
<li class="blockList">
<!-- ============ FIELD DETAIL =========== -->
<ul class="blockList">
<li class="blockList"><a name="field_detail">
<!--   -->
</a>
<h3>Field Detail</h3>
<a name="DV_ORDER">
<!--   -->
</a>
<ul class="blockListLast">
<li class="blockList">
<h4>DV_ORDER</h4>
<pre>public static&nbsp;java.util.Comparator&lt;? super <a href="../../mmj/lang/Var.html" title="class in mmj.lang">Var</a>&gt; DV_ORDER</pre>
<div class="block">This is the ordering that will be used to determine which variable in a
 DjVars is "hi" and which is "lo", and is visible to the user as the
 ordering of variables in missing $d statmements generated by the program.
 This comparator sorts by the standard ASCII string comparison on the
 labels, but sorts set variables before other things. If the .mm file that
 is loaded does not have a type code called "set", this is just a plain
 ASCII sort.</div>
</li>
</ul>
</li>
</ul>
<!-- ========= CONSTRUCTOR DETAIL ======== -->
<ul class="blockList">
<li class="blockList"><a name="constructor_detail">
<!--   -->
</a>
<h3>Constructor Detail</h3>
<a name="DjVars(java.util.Map, java.lang.String, java.lang.String)">
<!--   -->
</a>
<ul class="blockList">
<li class="blockList">
<h4>DjVars</h4>
<pre>public&nbsp;DjVars(java.util.Map&lt;java.lang.String,<a href="../../mmj/lang/Sym.html" title="class in mmj.lang">Sym</a>&gt;&nbsp;symTbl,
      java.lang.String&nbsp;loS,
      java.lang.String&nbsp;hiS)
       throws <a href="../../mmj/lang/LangException.html" title="class in mmj.lang">LangException</a></pre>
<div class="block">Construct using two Var id Strings. The input variables are validated and
 switched if necessary into varLo and varHi based on Var.id. Note: it is
 required that the Var's specified be "active", but not that there be
 active VarHyp's associated with them. The $d vars on an Assrt may be
 specified for use in a proof step, and it is guaranteed that that proof
 step will have its own VarHyp's (or else there would be a different
 error.)</div>
<dl><dt><span class="strong">Parameters:</span></dt><dd><code>symTbl</code> - Symbol Table (Map)</dd><dd><code>loS</code> - Var1 id String.</dd><dd><code>hiS</code> - Var2 id String.</dd>
<dt><span class="strong">Throws:</span></dt>
<dd><code><a href="../../mmj/lang/LangException.html" title="class in mmj.lang">LangException</a></code> - if the two Var id's are identical, or are not
             defined and active vars.</dd></dl>
</li>
</ul>
<a name="DjVars(mmj.lang.Var, mmj.lang.Var)">
<!--   -->
</a>
<ul class="blockListLast">
<li class="blockList">
<h4>DjVars</h4>
<pre>public&nbsp;DjVars(<a href="../../mmj/lang/Var.html" title="class in mmj.lang">Var</a>&nbsp;lo,
      <a href="../../mmj/lang/Var.html" title="class in mmj.lang">Var</a>&nbsp;hi)
       throws <a href="../../mmj/lang/LangException.html" title="class in mmj.lang">LangException</a></pre>
<div class="block">Construct using two Var's. The input variables are compared and switched
 if necessary into varLo and varHi based on Var.id.</div>
<dl><dt><span class="strong">Parameters:</span></dt><dd><code>lo</code> - Var 1.</dd><dd><code>hi</code> - Var 2.</dd>
<dt><span class="strong">Throws:</span></dt>
<dd><code><a href="../../mmj/lang/LangException.html" title="class in mmj.lang">LangException</a></code> - if the two Var id's are identical.</dd></dl>
</li>
</ul>
</li>
</ul>
<!-- ============ METHOD DETAIL ========== -->
<ul class="blockList">
<li class="blockList"><a name="method_detail">
<!--   -->
</a>
<h3>Method Detail</h3>
<a name="areBothDjVarsInExtendedFrame(mmj.lang.DjVars, mmj.lang.ScopeFrame, mmj.lang.ScopeFrame)">
<!--   -->
</a>
<ul class="blockList">
<li class="blockList">
<h4>areBothDjVarsInExtendedFrame</h4>
<pre>public static&nbsp;boolean&nbsp;areBothDjVarsInExtendedFrame(<a href="../../mmj/lang/DjVars.html" title="class in mmj.lang">DjVars</a>&nbsp;djVars,
                                   <a href="../../mmj/lang/ScopeFrame.html" title="class in mmj.lang">ScopeFrame</a>&nbsp;mandFrame,
                                   <a href="../../mmj/lang/ScopeFrame.html" title="class in mmj.lang">ScopeFrame</a>&nbsp;optFrame)</pre>
<div class="block">Helper routine for Theorem Loader to confirm that both DjVars variables
 are in the Extended Frame of a theorem.</div>
<dl><dt><span class="strong">Parameters:</span></dt><dd><code>djVars</code> - DjVars object to check.</dd><dd><code>mandFrame</code> - Mandatory Frame from a Theorem.</dd><dd><code>optFrame</code> - Optional Frame from a Theorem.</dd>
<dt><span class="strong">Returns:</span></dt><dd>true if both DjVars variables are used in VarHyps in the Extended
         Frame, otherwise false.</dd></dl>
</li>
</ul>
<a name="isDjVarsVarInExtendedFrame(mmj.lang.Var, mmj.lang.ScopeFrame, mmj.lang.ScopeFrame)">
<!--   -->
</a>
<ul class="blockList">
<li class="blockList">
<h4>isDjVarsVarInExtendedFrame</h4>
<pre>public static&nbsp;boolean&nbsp;isDjVarsVarInExtendedFrame(<a href="../../mmj/lang/Var.html" title="class in mmj.lang">Var</a>&nbsp;djVarsVar,
                                 <a href="../../mmj/lang/ScopeFrame.html" title="class in mmj.lang">ScopeFrame</a>&nbsp;mandFrame,
                                 <a href="../../mmj/lang/ScopeFrame.html" title="class in mmj.lang">ScopeFrame</a>&nbsp;optFrame)</pre>
<div class="block">Helper routine for Proof Assistant to confirm that a DjVars variable is
 defined in the Theorem's Extended Frame.</div>
<dl><dt><span class="strong">Parameters:</span></dt><dd><code>djVarsVar</code> - variable object to check.</dd><dd><code>mandFrame</code> - Mandatory Frame from a Theorem.</dd><dd><code>optFrame</code> - Optional Frame from a Theorem.</dd>
<dt><span class="strong">Returns:</span></dt><dd>true if both DjVars variables are used in VarHyps in the Extended
         Frame, otherwise false.</dd></dl>
</li>
</ul>
<a name="buildMetamathDjVarsStatementList(mmj.pa.DistinctVariablesStmt[])">
<!--   -->
</a>
<ul class="blockList">
<li class="blockList">
<h4>buildMetamathDjVarsStatementList</h4>
<pre>public static&nbsp;java.util.List&lt;java.lang.StringBuilder&gt;&nbsp;buildMetamathDjVarsStatementList(<a href="../../mmj/pa/DistinctVariablesStmt.html" title="class in mmj.pa">DistinctVariablesStmt</a>[]&nbsp;distinctVariablesStmtArray)</pre>
<div class="block">Builds a LinkedList of StringBuilders containing the Metamath formatted
 text $d statements for the theorem.
 <p>
 The input DistinctVariablesStmt array objects are consolidated to remove
 duplicates, sorted and then merged to create a concise set of $d
 statements.</div>
<dl><dt><span class="strong">Parameters:</span></dt><dd><code>distinctVariablesStmtArray</code> - array of Proof Worksheet
            DistinctVariablesStmt objects.</dd>
<dt><span class="strong">Returns:</span></dt><dd>List of StringBuilders containing $d statements (not containing
         any newlines).</dd></dl>
</li>
</ul>
<a name="buildMetamathDjVarsStatementList(mmj.lang.Theorem)">
<!--   -->
</a>
<ul class="blockList">
<li class="blockList">
<h4>buildMetamathDjVarsStatementList</h4>
<pre>public static&nbsp;java.util.List&lt;java.lang.StringBuilder&gt;&nbsp;buildMetamathDjVarsStatementList(<a href="../../mmj/lang/Theorem.html" title="class in mmj.lang">Theorem</a>&nbsp;theorem)</pre>
<div class="block">Builds a LinkedList of StringBuilders containing the Metamath format text
 $d statements for the theorem.</div>
<dl><dt><span class="strong">Parameters:</span></dt><dd><code>theorem</code> - the theorem for which $d statements are needed.</dd>
<dt><span class="strong">Returns:</span></dt><dd>List of StringBuilders containing $d statements (not containing
         any newlines).</dd></dl>
</li>
</ul>
<a name="convertDvGroupsListToMetamathList(java.util.List)">
<!--   -->
</a>
<ul class="blockList">
<li class="blockList">
<h4>convertDvGroupsListToMetamathList</h4>
<pre>public static&nbsp;java.util.List&lt;java.lang.StringBuilder&gt;&nbsp;convertDvGroupsListToMetamathList(java.util.List&lt;java.util.List&lt;<a href="../../mmj/lang/Var.html" title="class in mmj.lang">Var</a>&gt;&gt;&nbsp;comboDvGroups)</pre>
<div class="block">Converts a ArrayList of Lists containing distinct variables into a
 LinkedList of StringBuilders containing Metamath format text $d
 statements.</div>
<dl><dt><span class="strong">Parameters:</span></dt><dd><code>comboDvGroups</code> - List of Lists containing distinct variables.</dd>
<dt><span class="strong">Returns:</span></dt><dd>List of StringBuilders containing $d statements not containing
         any newlines.</dd></dl>
</li>
</ul>
<a name="sortAndCombineDvArrays(mmj.lang.DjVars[], mmj.lang.DjVars[])">
<!--   -->
</a>
<ul class="blockList">
<li class="blockList">
<h4>sortAndCombineDvArrays</h4>
<pre>public static&nbsp;<a href="../../mmj/lang/DjVars.html" title="class in mmj.lang">DjVars</a>[]&nbsp;sortAndCombineDvArrays(<a href="../../mmj/lang/DjVars.html" title="class in mmj.lang">DjVars</a>[]&nbsp;array1,
                              <a href="../../mmj/lang/DjVars.html" title="class in mmj.lang">DjVars</a>[]&nbsp;array2)</pre>
<div class="block">Merges two arrays of DjVars returning a single array in ascending
 compareTo order with duplicates eliminated.</div>
<dl><dt><span class="strong">Parameters:</span></dt><dd><code>array1</code> - 1st array of DjVars objects, may be null.</dd><dd><code>array2</code> - 2nd array of DjVars objects, may be null.</dd>
<dt><span class="strong">Returns:</span></dt><dd>consolidated, sorted array of DjVars objects.</dd></dl>
</li>
</ul>
<a name="sortAndCombineDvListOfLists(java.util.List)">
<!--   -->
</a>
<ul class="blockList">
<li class="blockList">
<h4>sortAndCombineDvListOfLists</h4>
<pre>public static&nbsp;<a href="../../mmj/lang/DjVars.html" title="class in mmj.lang">DjVars</a>[]&nbsp;sortAndCombineDvListOfLists(java.util.List&lt;java.util.List&lt;<a href="../../mmj/lang/DjVars.html" title="class in mmj.lang">DjVars</a>&gt;&gt;&nbsp;list1)</pre>
<div class="block">Merges lists of lists of DjVars returning a single array in ascending
 compareTo order with duplicates eliminated.</div>
<dl><dt><span class="strong">Parameters:</span></dt><dd><code>list1</code> - List containing List elements of DjVars objects.</dd>
<dt><span class="strong">Returns:</span></dt><dd>consolidated, sorted array of DjVars objects.</dd></dl>
</li>
</ul>
<a name="set(mmj.lang.Var, mmj.lang.Var)">
<!--   -->
</a>
<ul class="blockList">
<li class="blockList">
<h4>set</h4>
<pre>public&nbsp;void&nbsp;set(<a href="../../mmj/lang/Var.html" title="class in mmj.lang">Var</a>&nbsp;lo,
       <a href="../../mmj/lang/Var.html" title="class in mmj.lang">Var</a>&nbsp;hi)
         throws <a href="../../mmj/lang/LangException.html" title="class in mmj.lang">LangException</a></pre>
<div class="block">Set the contents of this DjVars object. The input variables are compared
 and switched if necessary into varLo and varHi based on Var.id.</div>
<dl><dt><span class="strong">Parameters:</span></dt><dd><code>lo</code> - Var 1.</dd><dd><code>hi</code> - Var 2.</dd>
<dt><span class="strong">Throws:</span></dt>
<dd><code><a href="../../mmj/lang/LangException.html" title="class in mmj.lang">LangException</a></code> - if the two Var id's are identical.</dd></dl>
</li>
</ul>
<a name="getVarLo()">
<!--   -->
</a>
<ul class="blockList">
<li class="blockList">
<h4>getVarLo</h4>
<pre>public&nbsp;<a href="../../mmj/lang/Var.html" title="class in mmj.lang">Var</a>&nbsp;getVarLo()</pre>
<div class="block">Return the "low" Dj Var, varLo.</div>
<dl><dt><span class="strong">Returns:</span></dt><dd>varLo the "low" Var based on Var.id.</dd></dl>
</li>
</ul>
<a name="getVarHi()">
<!--   -->
</a>
<ul class="blockList">
<li class="blockList">
<h4>getVarHi</h4>
<pre>public&nbsp;<a href="../../mmj/lang/Var.html" title="class in mmj.lang">Var</a>&nbsp;getVarHi()</pre>
<div class="block">Return the "high" Dj Var, varHi.</div>
<dl><dt><span class="strong">Returns:</span></dt><dd>varHi the "high" Var based on Var.id.</dd></dl>
</li>
</ul>
<a name="toString()">
<!--   -->
</a>
<ul class="blockList">
<li class="blockList">
<h4>toString</h4>
<pre>public&nbsp;java.lang.String&nbsp;toString()</pre>
<div class="block">Converts DjVars to String.</div>
<dl>
<dt><strong>Overrides:</strong></dt>
<dd><code>toString</code>&nbsp;in class&nbsp;<code>java.lang.Object</code></dd>
<dt><span class="strong">Returns:</span></dt><dd>returns DjVars string;</dd></dl>
</li>
</ul>
<a name="hashCode()">
<!--   -->
</a>
<ul class="blockList">
<li class="blockList">
<h4>hashCode</h4>
<pre>public&nbsp;int&nbsp;hashCode()</pre>
<dl>
<dt><strong>Overrides:</strong></dt>
<dd><code>hashCode</code>&nbsp;in class&nbsp;<code>java.lang.Object</code></dd>
</dl>
</li>
</ul>
<a name="equals(java.lang.Object)">
<!--   -->
</a>
<ul class="blockList">
<li class="blockList">
<h4>equals</h4>
<pre>public&nbsp;boolean&nbsp;equals(java.lang.Object&nbsp;obj)</pre>
<dl>
<dt><strong>Overrides:</strong></dt>
<dd><code>equals</code>&nbsp;in class&nbsp;<code>java.lang.Object</code></dd>
</dl>
</li>
</ul>
<a name="compareTo(mmj.lang.DjVars)">
<!--   -->
</a>
<ul class="blockListLast">
<li class="blockList">
<h4>compareTo</h4>
<pre>public&nbsp;int&nbsp;compareTo(<a href="../../mmj/lang/DjVars.html" title="class in mmj.lang">DjVars</a>&nbsp;obj)</pre>
<div class="block">Compares DjVars object based on the variables.</div>
<dl>
<dt><strong>Specified by:</strong></dt>
<dd><code>compareTo</code>&nbsp;in interface&nbsp;<code>java.lang.Comparable&lt;<a href="../../mmj/lang/DjVars.html" title="class in mmj.lang">DjVars</a>&gt;</code></dd>
<dt><span class="strong">Parameters:</span></dt><dd><code>obj</code> - Order object to compare to this Order</dd>
<dt><span class="strong">Returns:</span></dt><dd>returns negative, zero, or a positive int if this Order object is
         less than, equal to or greater than the input parameter obj.</dd></dl>
</li>
</ul>
</li>
</ul>
</li>
</ul>
</div>
</div>
<!-- ========= END OF CLASS DATA ========= -->
<!-- ======= START OF BOTTOM NAVBAR ====== -->
<div class="bottomNav"><a name="navbar_bottom">
<!--   -->
</a><a href="#skip-navbar_bottom" title="Skip navigation links"></a><a name="navbar_bottom_firstrow">
<!--   -->
</a>
<ul class="navList" title="Navigation">
<li><a href="../../overview-summary.html">Overview</a></li>
<li><a href="package-summary.html">Package</a></li>
<li class="navBarCell1Rev">Class</li>
<li><a href="package-tree.html">Tree</a></li>
<li><a href="../../deprecated-list.html">Deprecated</a></li>
<li><a href="../../index-all.html">Index</a></li>
<li><a href="../../help-doc.html">Help</a></li>
</ul>
</div>
<div class="subNav">
<ul class="navList">
<li><a href="../../mmj/lang/Cnst.html" title="class in mmj.lang"><span class="strong">Prev Class</span></a></li>
<li><a href="../../mmj/lang/Formula.html" title="class in mmj.lang"><span class="strong">Next Class</span></a></li>
</ul>
<ul class="navList">
<li><a href="../../index.html?mmj/lang/DjVars.html" target="_top">Frames</a></li>
<li><a href="DjVars.html" target="_top">No Frames</a></li>
</ul>
<ul class="navList" id="allclasses_navbar_bottom">
<li><a href="../../allclasses-noframe.html">All Classes</a></li>
</ul>
<div>
<script type="text/javascript"><!--
  allClassesLink = document.getElementById("allclasses_navbar_bottom");
  if(window==top) {
    allClassesLink.style.display = "block";
  }
  else {
    allClassesLink.style.display = "none";
  }
  //-->
</script>
</div>
<div>
<ul class="subNavList">
<li>Summary:&nbsp;</li>
<li>Nested&nbsp;|&nbsp;</li>
<li><a href="#field_summary">Field</a>&nbsp;|&nbsp;</li>
<li><a href="#constructor_summary">Constr</a>&nbsp;|&nbsp;</li>
<li><a href="#method_summary">Method</a></li>
</ul>
<ul class="subNavList">
<li>Detail:&nbsp;</li>
<li><a href="#field_detail">Field</a>&nbsp;|&nbsp;</li>
<li><a href="#constructor_detail">Constr</a>&nbsp;|&nbsp;</li>
<li><a href="#method_detail">Method</a></li>
</ul>
</div>
<a name="skip-navbar_bottom">
<!--   -->
</a></div>
<!-- ======== END OF BOTTOM NAVBAR ======= -->
</body>
</html>
